E:Type, pred?:(E(E+Unit)), e:E.
SWellFounded(first(y) & x = pred(y)  E)  eventlist(pred?;e)  E List 

latex

Definitions	x:A. B(x), P  Q, A & B, t  T, x,y. t(x;y), A, ij, AB, False, Prop, eventlist(pred?;e), Y, if b t else f fi, true, false, SWellFounded(R(x;y)), x:A. B(x), , x(s1,s2), Unit, , P  Q, P & Q,
Lemmas	nat wf, strongwellfounded wf, not wf, assert wf, first wf, pred wf, unit wf, nat properties, ge wf, bool wf, eqtt to assert, iff transitivity, bnot wf, eqff to assert, assert of bnot, append wf